T:Type, l:(T List), i:, j:{0..||l||}, x:T.
l[i:=x][j] = if (j = i) then x else l[j] fi   T 

latex

Definitions	t  T, x:A. B(x), ||as||, P & Q, i  j < k, P  Q, False, A, A  B, {i..j}, l[i], (i = j), if b then t else f fi , , P  Q, P  Q, f[x:=v], l[i:=x]
Lemmas	mklist select, le wf, int seg wf, ifthenelse wf, eq int wf, select wf, length wf1